1  /-
  2  Copyright (c) 2019 Sébastien Gouëzel. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Sébastien Gouëzel
  5  -/
  6  
  7  import topology.metric_space.basic analysis.specific_limits
src         └─────────────────────────┘ └──────────────────────┘
  8  
  9  /-!
 10  # Baire theorem
 11  
 12  In a complete metric space, a countable intersection of dense open subsets is dense.
 13  
 14  The good concept underlying the theorem is that of a Gδ set, i.e., a countable intersection
 15  of open sets. Then Baire theorem can also be formulated as the fact that a countable
 16  intersection of dense Gδ sets is a dense Gδ set. We prove Baire theorem, giving several different
 17  formulations that can be handy. We also prove the important consequence that, if the space is
 18  covered by a countable union of closed sets, then the union of their interiors is dense.
 19  
 20  The names of the theorems do not contain the string "Baire", but are instead built from the form of
 21  the statement. "Baire" is however in the docstring of all the theorems, to facilitate grep searches.
 22  -/
 23  
 24  noncomputable theory
 25  open_locale classical
 26  
 27  open filter lattice encodable set
 28  
 29  variables {α : Type*} {β : Type*} {γ : Type*}
 30  
 31  section is_Gδ
 32  variable [topological_space α]
id             └───────────────┘
src            └───────────────┘
typ            └───────────────┘
doc            └───────────────┘
 33  
 34  /-- A Gδ set is a countable intersection of open sets. -/
 35  def is_Gδ (s : set α) : Prop :=
id                  └─┘ 
src                 └─┘
typ                 └─┘ 
 36    ∃T : set (set α), (∀t ∈ T, is_open t) ∧ countable T ∧ s = (⋂₀ T)
id         └─┘  └─┘          └─────┘    └───────┘      └┘ 
src        └─┘  └─┘            └─────┘     └───────┘        └┘
typ        └─┘  └─┘          └─────┘    └───────┘      └┘ 
doc                               └─────┘      └───────┘          └┘
 37  
 38  /-- An open set is a Gδ set. -/
 39  lemma is_open.is_Gδ {s : set α} (h : is_open s) : is_Gδ s :=
id                            └─┘        └─────┘     └───┘ 
src                           └─┘         └─────┘      └───┘
typ                           └─┘        └─────┘     └───┘ 
doc                                       └─────┘      └───┘
 40  ⟨{s}, by simp [h], countable_singleton _, (set.sInter_singleton _).symm⟩
id                      └─────────────────┘     └──────────────────┘
src           └────┘   └─────────────────┘     └──────────────────┘
typ           └────┘   └─────────────────┘     └──────────────────┘
doc           └────┘ 
txt           └────┘ 
par           └────┘ 
pid                
 41  
 42  lemma is_Gδ_bInter_of_open {ι : Type*} {I : set ι} (hI : countable I) {f : ι → set α}
 43    (hf : ∀i ∈ I, is_open (f i)) : is_Gδ (⋂i∈I, f i) :=
 44  ⟨f '' I, by rwa ball_image_iff, countable_image _ hI, by rw sInter_image⟩
src              └──┘                                         └─┘
typ              └──┘                                         └─┘
doc              └──┘                                         └─┘
txt              └──┘                                         └─┘
par              └──┘                                         └─┘
pid                                                            
 45  
 46  lemma is_Gδ_Inter_of_open {ι : Type*} [encodable ι] {f : ι → set α}
 47    (hf : ∀i, is_open (f i)) : is_Gδ (⋂i, f i) :=
id                               └───┘    
src                               └───┘   
typ                              └───┘    
doc                               └───┘   
 48  ⟨range f, by rwa forall_range_iff, countable_range _, by rw sInter_range⟩
id    └───┘          └──────────────┘  └─────────────┘          └──────────┘
src   └───┘       └──┘└──────────────┘  └─────────────┘       └─┘└──────────┘
typ   └───┘      └──┘└──────────────┘  └─────────────┘       └─┘└──────────┘
doc   └───┘       └──┘                                        └─┘
txt               └──┘                                        └─┘
par               └──┘                                        └─┘
pid                                                            
st               └───────────────────┘                       └──────────────┘
 49  
 50  /-- A countable intersection of Gδ sets is a Gδ set. -/
 51  lemma is_Gδ_sInter {S : set (set α)} (h : ∀s∈S, is_Gδ s) (hS : countable S) : is_Gδ (⋂₀ S) :=
id                           └─┘  └─┘             └───┘         └───────┘     └───┘  └┘ 
src                          └─┘  └─┘                └───┘          └───────┘      └───┘  └┘
typ                          └─┘  └─┘             └───┘         └───────┘     └───┘  └┘ 
doc                                                  └───┘          └───────┘      └───┘  └┘
 52  begin
 53    have : ∀s : set α, ∃T : set (set α), s ∈ S → ((∀t ∈ T, is_open t) ∧ countable T ∧ s = (⋂₀ T)),
id                             └─┘  └─┘                   └─────┘     └───────┘         └┘
src    └─────┘ └──┘      └──┘    └─┘        └──┘  └─────┘ └┘└───────┘    └┘ └┘
typ    └─────┘ └──┘      └──┘└─┘ └─┘     └──┘  └─────┘ └┘└───────┘    └┘ └┘
doc    └─────┘ └──┘      └──┘                └──┘  └─────┘ └┘ └───────┘     └┘ └┘
txt    └─────┘ └──┘      └──┘                └──┘          └┘                  └┘
par    └─────┘ └──┘      └──┘                └──┘          └┘                  └┘
pid    └───┘└┘ └──┘      └──┘                └──┘          └┘                  └┘
st                           └─────────────────────────────────────────────────────────────────────┘└─
 54    { assume s,
src      └──────┘
typ      └──────┘
doc      └──────┘
txt      └──────┘
par      └──────┘
pid      └──────┘
st   ───┘└──────┘└─
 55      by_cases hs : s ∈ S,
id                        
src      └───────┘  └─┘  
typ      └───────┘  └─┘ 
doc      └───────┘  └─┘  
txt      └───────┘  └─┘  
par      └───────┘  └─┘  
pid                └─┘  
st   ──────────────────────┘└─
 56      { simp [hs], exact h s hs },
id               └┘           └┘
src        └────┘    └────┘    
typ        └────┘└┘  └────┘└┘
doc        └────┘    └────┘    
txt        └────┘    └────┘    
par        └────┘    └────┘    
pid                         
st   ─────┘└───────┘└─────────────┘└┘
 57      { simp [hs] }},
id               └┘
src        └────┘  └┘
typ        └────┘└┘└┘
doc        └────┘  └┘
txt        └────┘  └┘
par        └────┘  └┘
pid              
st   ───────────────┘└─┘
 58    choose T hT using this,
id                       └──┘
src    └────────────────┘
typ    └────────────────┘└──┘
doc    └────────────────┘
txt    └────────────────┘
par    └────────────────┘
pid          └┘└─┘└─────┘
st   ───────────────────────┘└─
 59    refine ⟨⋃s∈S, T s, λt ht, _, _, _⟩,
id                
src    └─────┘ └┘   └┘ └────────────┘
typ    └─────┘ └┘ └┘ └────────────┘
doc    └─────┘ └┘   └┘ └────────────┘
txt    └─────┘  └┘    └┘ └────────────┘
par    └─────┘  └┘    └┘ └────────────┘
pid            └┘    └┘ └────────────┘
st   ───────────────────────────────────┘└─
 60    { simp only [exists_prop, set.mem_Union] at ht,
id                  └─────────┘  └───────────┘
src      └─────────┘└─────────┘└┘└───────────┘└─────┘
typ      └─────────┘└─────────┘└┘└───────────┘└─────┘
doc      └─────────┘           └┘             └─────┘
txt      └─────────┘           └┘             └─────┘
par      └─────────┘           └┘             └─────┘
pid          └──┘└┘           └┘             └───┘
st   ───┘└──────────────────────────────────────────┘└─
 61      rcases ht with ⟨s, hs, tTs⟩,
id              └┘
src      └─────┘  └────────────────┘
typ      └─────┘└┘└────────────────┘
doc      └─────┘  └────────────────┘
txt      └─────┘  └────────────────┘
par      └─────┘  └────────────────┘
pid              └────────────────┘
st   ──────────────────────────────┘└─
 62      exact (hT s hs).1 t tTs },
id              └┘  └┘     └─┘
src      └────┘      └──┘    
typ      └────┘ └┘└┘└──┘└─┘
doc      └────┘      └──┘    
txt      └────┘      └──┘    
par      └────┘      └──┘    
pid                 └──┘    
st   ───────────────────────────┘└┘
 63    { exact countable_bUnion hS (λs hs, (hT s hs).2.1) },
id             └──────────────┘ └┘          └┘
src      └────┘└──────────────┘    └────┘      └─────┘
typ      └────┘└──────────────┘└┘  └────┘ └┘   └─────┘
doc      └────┘                    └────┘      └─────┘
txt      └────┘                    └────┘      └─────┘
par      └────┘                    └────┘      └─────┘
pid                               └────┘      └────┘
st   ───┘└───────────────────────────────────────────────┘└┘
 64    { exact (sInter_bUnion (λs hs, (hT s hs).2.2)).symm }
id              └───────────┘          └┘
src      └────┘ └───────────┘  └────┘      └───────────┘
typ      └────┘ └───────────┘  └────┘ └┘   └───────────┘
doc      └────┘                └────┘      └───────────┘
txt      └────┘                └────┘      └───────────┘
par      └────┘                └────┘      └───────────┘
pid                           └────┘      └─────────┘└┘
st   ─────────────────────────────────────────────────────┘└─
 65  end
st   ──┘
 66  
 67  /-- The union of two Gδ sets is a Gδ set. -/
 68  lemma is_Gδ.union {s t : set α} (hs : is_Gδ s) (ht : is_Gδ t) : is_Gδ (s ∪ t) :=
id                            └─┘         └───┘         └───┘     └───┘    
src                           └─┘          └───┘          └───┘      └───┘    
typ                           └─┘         └───┘         └───┘     └───┘    
doc                                        └───┘          └───┘      └───┘
 69  begin
st   └─────
 70    rcases hs with ⟨S, Sopen, Scount, sS⟩,
id            └┘
src    └─────┘  └──────────────────────────┘
typ    └─────┘└┘└──────────────────────────┘
doc    └─────┘  └──────────────────────────┘
txt    └─────┘  └──────────────────────────┘
par    └─────┘  └──────────────────────────┘
pid            └──────────────────────────┘
st   ──────────────────────────────────────┘└─
 71    rcases ht with ⟨T, Topen, Tcount, tT⟩,
id            └┘
src    └─────┘  └──────────────────────────┘
typ    └─────┘└┘└──────────────────────────┘
doc    └─────┘  └──────────────────────────┘
txt    └─────┘  └──────────────────────────┘
par    └─────┘  └──────────────────────────┘
pid            └──────────────────────────┘
st   ──────────────────────────────────────┘└─
 72    rw [sS, tT, sInter_union_sInter],
id         └┘  └┘  └─────────────────┘
src    └──┘  └┘  └┘└─────────────────┘
typ    └──┘└┘└┘└┘└┘└─────────────────┘
doc    └──┘  └┘  └┘                   
txt    └──┘  └┘  └┘                   
par    └──┘  └┘  └┘                   
pid      └┘  └┘  └┘                   
st   ───────┘└──┘└───────────────────┘└──
 73    apply is_Gδ_bInter_of_open (countable_prod Scount Tcount),
id           └──────────────────┘  └────────────┘ └────┘ └────┘
src    └────┘└──────────────────┘ └────────────┘            
typ    └────┘└──────────────────┘ └────────────┘└────┘└────┘
doc    └────┘                                               
txt    └────┘                                               
par    └────┘                                               
pid                                                        
st   ──────────────────────────────────────────────────────────┘└─
 74    rintros ⟨a, b⟩ hab,
src    └────────────────┘
typ    └────────────────┘
doc    └────────────────┘
txt    └────────────────┘
par    └────────────────┘
pid           └─────────┘
st   ───────────────────┘└─
 75    simp only [set.prod_mk_mem_set_prod_eq] at hab,
id                └─────────────────────────┘
src    └─────────┘└─────────────────────────┘└──────┘
typ    └─────────┘└─────────────────────────┘└──────┘
doc    └─────────┘                           └──────┘
txt    └─────────┘                           └──────┘
par    └─────────┘                           └──────┘
pid        └──┘└┘                           └────┘
st   ───────────────────────────────────────────────┘└─
 76    have aopen : is_open a := Sopen a hab.1,
id                  └─────┘     └───┘  └─┘
src    └───────────┘└─────┘ └──┘         └┘
typ    └───────────┘└─────┘└──┘└───┘└─┘└┘
doc    └───────────┘└─────┘ └──┘         └┘
txt    └───────────┘        └──┘         └┘
par    └───────────┘        └──┘         └┘
pid    └────────┘└─┘        └──┘         └┘
st   ────────────────────────────────────────┘└─
 77    have bopen : is_open b := Topen b hab.2,
id                  └─────┘     └───┘  └─┘
src    └───────────┘└─────┘ └──┘         └┘
typ    └───────────┘└─────┘└──┘└───┘└─┘└┘
doc    └───────────┘└─────┘ └──┘         └┘
txt    └───────────┘        └──┘         └┘
par    └───────────┘        └──┘         └┘
pid    └────────┘└─┘        └──┘         └┘
st   ────────────────────────────────────────┘└─
 78    simp [aopen, bopen, is_open_union]
id           └───┘  └───┘  └───────────┘
src    └────┘     └┘     └┘└───────────┘└┘
typ    └────┘└───┘└┘└───┘└┘└───────────┘└┘
doc    └────┘     └┘     └┘             └┘
txt    └────┘     └┘     └┘             └┘
par    └────┘     └┘     └┘             └┘
pid             └┘     └┘             
st   ────────────────────────────────────┘
 79  end
st   └─┘
 80  
 81  end is_Gδ
 82  
 83  section Baire_theorem
 84  open metric
 85  variables [metric_space α] [complete_space α]
id              └──────────┘     └────────────┘
src             └──────────┘     └────────────┘
typ             └──────────┘     └────────────┘
doc             └──────────┘     └────────────┘
 86  
 87  /-- Baire theorem: a countable intersection of dense open sets is dense. Formulated here when
 88  the source space is ℕ (and subsumed below by `dense_Inter_of_open` working with any
 89  encodable source space). -/
 90  theorem dense_Inter_of_open_nat {f : ℕ → set α} (ho : ∀n, is_open (f n))
id                                           └─┘            └─────┘   
src                                          └─┘              └─────┘
typ                                          └─┘            └─────┘   
doc                                                            └─────┘
 91    (hd : ∀n, closure (f n) = univ) : closure (⋂n, f n) = univ :=
id              └─────┘      └──┘    └─────┘       └──┘
src              └─────┘        └──┘    └─────┘          └──┘
typ             └─────┘      └──┘    └─────┘       └──┘
doc              └─────┘                 └─────┘   
 92  begin
st   └─────
 93    let B : ℕ → ℝ := λn, ((1/2)^n : ℝ),
id                              
src    └──────┘  └──┘ └─┘  └┘ └─┘ 
typ    └──────┘  └──┘ └─┘  └┘ └─┘ 
doc    └──────┘   └──┘ └─┘   └┘  └─┘ 
txt    └──────┘   └──┘ └─┘   └┘  └─┘ 
par    └──────┘   └──┘ └─┘   └┘  └─┘ 
pid    └───┘└─┘   └──┘ └─┘   └┘  └─┘ 
st   ───────────────────────────────────┘└─
 94    have Bpos : ∀n, 0 < B n := λn, begin apply pow_pos, by norm_num end,
id                                              └─────┘
src    └──────────┘  └─┘  └──┘ └─┘     └────┘└─────┘└───┘└───────┘└─┘
typ    └──────────┘  └─┘ └──┘ └─┘     └────┘└─────┘└───┘└───────┘└─┘
doc    └──────────┘  └─┘   └──┘ └─┘     └────┘       └───┘└───────┘└─┘
txt    └──────────┘  └─┘   └──┘ └─┘     └────┘       └───┘└───────┘└─┘
par    └──────────┘  └─┘   └──┘ └─┘     └────┘       └───┘└───────┘└─┘
pid    └───────┘└─┘  └─┘   └──┘ └─┘     └─────┘       └───────────────┘
st   ────────────────────────────────┘└─────────────────┘              └─┘└─
 95    /- Translate the density assumption into two functions `center` and `radius` associating
st   ───────────────────────────────────────────────────────────────────────────────────────────
 96    to any n, x, δ, δpos a center and a positive radius such that
st   ────────────────────────────────────────────────────────────────
 97    `closed_ball center radius` is included both in `f n` and in `closed_ball x δ`.
st   ──────────────────────────────────────────────────────────────────────────────────
 98    We can also require `radius ≤ (1/2)^(n+1), to ensure we get a Cauchy sequence later. -/
st   ──────────────────────────────────────────────────────────────────────────────────────────
 99    have : ∀n x δ, ∃y r, δ > 0 → (r > 0 ∧ r ≤ B (n+1) ∧ closed_ball y r ⊆ (closed_ball x δ) ∩ f n),
id                                                                    └─────────┘       
src    └─────┘ └───┘ └─┘ └─┘    └─┘    └─┘               └─────────┘  └┘  
typ    └─────┘ └───┘ └─┘ └─┘    └─┘   └─┘               └─────────┘  └┘ 
doc    └─────┘ └───┘  └─┘   └─┘    └─┘       └─┘                └─────────┘  └┘   
txt    └─────┘ └───┘  └─┘   └─┘    └─┘       └─┘                             └┘   
par    └─────┘ └───┘  └─┘   └─┘    └─┘       └─┘                             └┘   
pid    └───┘└┘ └───┘  └─┘   └─┘    └─┘       └─┘                             └┘   
st   ───────────────────────────────────────────────────────────────────────────────────────────────┘└─
100    { assume n x δ,
src      └──────────┘
typ      └──────────┘
doc      └──────────┘
txt      └──────────┘
par      └──────────┘
pid      └──────────┘
st   ───┘└──────────┘└─
101      by_cases δpos : δ > 0,
id                       
src      └───────┘    └─┘  └┘
typ      └───────┘    └─┘ └┘
doc      └───────┘    └─┘  └┘
txt      └───────┘    └─┘  └┘
par      └───────┘    └─┘  └┘
pid                  └─┘  
st   ────────────────────────┘└─
102      { have : x ∈ closure (f n) := by simpa only [(hd n).symm] using mem_univ x,
id                  └─────┘                        └┘               └──────┘ 
src        └─────┘ └─────┘   └───┘  └──────────┘    └────────────┘└──────┘
typ        └─────┘└─────┘ └───┘  └──────────┘ └┘└────────────┘└──────┘
doc        └─────┘  └─────┘   └───┘  └──────────┘    └────────────┘        
txt        └─────┘            └───┘  └──────────┘    └────────────┘        
par        └─────┘            └───┘  └──────────┘    └────────────┘        
pid        └───┘└┘            └──┘  └───────────┘    └────────────┘        
st   ─────┘└────────────────────────────┘└────────────────────────────────────────┘└─
103        rcases mem_closure_iff'.1 this (δ/2) (half_pos δpos) with ⟨y, ys, xy⟩,
id                └──────────────┘   └──┘       └──────┘ └──┘
src        └─────┘└──────────────┘└─┘       └─┘ └──────┘    └────────────────┘
typ        └─────┘└──────────────┘└─┘└──┘  └─┘ └──────┘└──┘└────────────────┘
doc        └─────┘└──────────────┘└─┘       └─┘             └────────────────┘
txt        └─────┘                └─┘       └─┘             └────────────────┘
par        └─────┘                └─┘       └─┘             └────────────────┘
pid                              └─┘       └─┘             └────────────────┘
st   ──────────────────────────────────────────────────────────────────────────┘└─
104        rw dist_comm at xy,
id            └───────┘
src        └─┘└───────┘└────┘
typ        └─┘└───────┘└────┘
doc        └─┘         └────┘
txt        └─┘         └────┘
par        └─┘         └────┘
pid                   └────┘
st   ───────────────────────┘└─
105        rcases is_open_iff.1 (ho n) y ys with ⟨r, rpos, hr⟩,
id                └─────────┘    └┘    └┘
src        └─────┘└─────────┘└─┘    └┘   └─────────────────┘
typ        └─────┘└─────────┘└─┘ └┘└┘└┘└─────────────────┘
doc        └─────┘           └─┘    └┘   └─────────────────┘
txt        └─────┘           └─┘    └┘   └─────────────────┘
par        └─────┘           └─┘    └┘   └─────────────────┘
pid                         └─┘    └┘   └─────────────────┘
st   ────────────────────────────────────────────────────────┘└─
106        refine ⟨y, min (min (δ/2) (r/2)) (B (n+1)), λ_, ⟨_, _, λz hz, ⟨_, _⟩⟩⟩,
id                        └─┘               
src        └─────┘  └┘    └─┘   └─┘   └──┘     └───┘ └─┘ └────┘ └────┘ └─────┘
typ        └─────┘ └┘    └─┘  └─┘  └──┘   └───┘ └─┘ └────┘ └────┘ └─────┘
doc        └─────┘  └┘          └─┘   └──┘     └───┘ └─┘ └────┘ └────┘ └─────┘
txt        └─────┘  └┘          └─┘   └──┘     └───┘ └─┘ └────┘ └────┘ └─────┘
par        └─────┘  └┘          └─┘   └──┘     └───┘ └─┘ └────┘ └────┘ └─────┘
pid                └┘          └─┘   └──┘     └───┘ └─┘ └────┘ └────┘ └─────┘
st   ───────────────────────────────────────────────────────────────────────────┘└─
107        show 0 < min (min (δ / 2) (r/2)) (B (n+1)),
id                       └─┘                 
src        └─────┘     └─┘   └──┘   └──┘     └─┘
typ        └─────┘     └─┘  └──┘  └──┘   └─┘
doc        └─────┘           └──┘   └──┘     └─┘
txt        └─────┘           └──┘   └──┘     └─┘
par        └─────┘           └──┘   └──┘     └─┘
pid        └─────┘           └──┘   └──┘     └─┘
st   ───────────────────────────────────────────────┘└─
108          from lt_min (lt_min (half_pos δpos) (half_pos rpos)) (Bpos (n+1)),
id                        └────┘           └──┘   └──────┘ └──┘    └──┘  
src          └───┘       └────┘             └┘ └──────┘    └─┘        └─┘
typ          └───┘       └────┘         └──┘└┘ └──────┘└──┘└─┘ └──┘  └─┘
doc          └───┘                          └┘             └─┘        └─┘
txt          └───┘                          └┘             └─┘        └─┘
par          └───┘                          └┘             └─┘        └─┘
pid          └───┘                          └┘             └─┘        └─┘
st   ────────────────────────────────────────────────────────────────────────┘└─
109        show min (min (δ / 2) (r/2)) (B (n+1)) ≤ B (n+1), from min_le_right _ _,
id                   └─┘                                      └──────────┘
src        └───┘    └─┘   └──┘   └──┘     └──┘     └┘  └───┘└──────────┘└──┘
typ        └───┘    └─┘  └──┘  └──┘     └──┘   └┘  └───┘└──────────┘└──┘
doc        └───┘          └──┘   └──┘     └──┘     └┘  └───┘            └──┘
txt        └───┘          └──┘   └──┘     └──┘     └┘  └───┘            └──┘
par        └───┘          └──┘   └──┘     └──┘     └┘  └───┘            └──┘
pid        └───┘          └──┘   └──┘     └──┘     └┘  └───┘            └──┘
st   ────────────────────────────────────────────────────────────────────────────┘└─
110        show z ∈ closed_ball x δ, from calc
id                 └─────────┘  
src        └───┘  └─────────┘    └───┘    
typ        └───┘ └─────────┘  └───┘    
doc        └───┘  └─────────┘    └───┘    
txt        └───┘                 └───┘    
par        └───┘                 └───┘    
pid        └───┘                 └───┘    
st   ──────────────────────────────────────────
111          dist z x ≤ dist z y + dist y x : dist_triangle _ _ _
id                                └──┘     └───────────┘
src  ───────┘              └──┘  └─┘└───────────┘└──────
typ  ───────┘             └──┘└─┘└───────────┘└──────
doc  ───────┘                    └─┘             └──────
txt  ───────┘                    └─┘             └──────
par  ───────┘                    └─┘             └──────
pid  ───────┘                    └─┘             └──────
st   ─────────────────────────────────────────────────────────────
112          ... ≤ (min (min (δ / 2) (r/2)) (B (n+1))) + (δ/2) : add_le_add hz (le_of_lt xy)
id                       └─┘                                            └┘  └──────┘ └┘
src  ───────────┘      └─┘   └──┘   └──┘     └───┘    └───┘             └──────┘  └─
typ  ───────────┘      └─┘   └──┘  └──┘   └───┘   └───┘          └┘ └──────┘└┘└─
doc  ───────────┘            └──┘   └──┘     └───┘    └───┘                       └─
txt  ───────────┘            └──┘   └──┘     └───┘    └───┘                       └─
par  ───────────┘            └──┘   └──┘     └───┘    └───┘                       └─
pid  ───────────┘            └──┘   └──┘     └───┘    └───┘                       └─
st   ────────────────────────────────────────────────────────────────────────────────────────
113          ... ≤ δ/2 + δ/2 : add_le_add (le_trans (min_le_left _ _) (min_le_left _ _)) (le_refl _)
id                             └────────┘  └──────┘                    └─────────┘        └─────┘
src  ───────────┘   └┘   └──┘└────────┘ └──────┘            └────┘ └─────────┘└─────┘ └─────┘└───
typ  ───────────┘   └┘   └──┘└────────┘ └──────┘            └────┘ └─────────┘└─────┘ └─────┘└───
doc  ───────────┘   └┘   └──┘                               └────┘            └─────┘        └───
txt  ───────────┘   └┘   └──┘                               └────┘            └─────┘        └───
par  ───────────┘   └┘   └──┘                               └────┘            └─────┘        └───
pid  ───────────┘   └┘   └──┘                               └────┘            └─────┘        └───
st   ────────────────────────────────────────────────────────────────────────────────────────────────
114          ... = δ : add_halves _,
id                     └────────┘
src  ───────────┘  └─┘└────────┘└┘
typ  ───────────┘  └─┘└────────┘└┘
doc  ───────────┘  └─┘          └┘
txt  ───────────┘  └─┘          └┘
par  ───────────┘  └─┘          └┘
pid  ───────────┘  └─┘          └┘
st   ─────────────────────────────┘└─
115        show z ∈ f n, from hr (calc
id                         └┘
src        └───┘      └───┘       
typ        └───┘   └───┘└┘     
doc        └───┘      └───┘       
txt        └───┘      └───┘       
par        └───┘      └───┘       
pid        └───┘      └───┘       
st   ──────────────────────────────────
116          dist z y ≤ min (min (δ / 2) (r/2)) (B (n+1)) : hz
id           └──┘          └─┘                        └┘
src  ───────┘└──┘       └─┘   └──┘   └──┘     └────┘  
typ  ───────┘└──┘     └─┘  └──┘  └──┘   └────┘└┘
doc  ───────┘                 └──┘   └──┘     └────┘  
txt  ───────┘                 └──┘   └──┘     └────┘  
par  ───────┘                 └──┘   └──┘     └────┘  
pid  ───────┘                 └──┘   └──┘     └────┘  
st   ──────────────────────────────────────────────────────────
117          ... ≤ r/2 : le_trans (min_le_left _ _) (min_le_right _ _)
id                       └──────┘  └─────────┘       └──────────┘
src  ───────────┘   └──┘└──────┘ └─────────┘└────┘ └──────────┘└─────
typ  ───────────┘   └──┘└──────┘ └─────────┘└────┘ └──────────┘└─────
doc  ───────────┘   └──┘                    └────┘             └─────
txt  ───────────┘   └──┘                    └────┘             └─────
par  ───────────┘   └──┘                    └────┘             └─────
pid  ───────────┘   └──┘                    └────┘             └─────
st   ──────────────────────────────────────────────────────────────────
118          ... < r : half_lt_self rpos) },
id                     └──────────┘ └──┘
src  ───────────┘  └─┘└──────────┘    └┘
typ  ───────────┘  └─┘└──────────┘└──┘└┘
doc  ───────────┘  └─┘                └┘
txt  ───────────┘  └─┘                └┘
par  ───────────┘  └─┘                └┘
pid  ───────────┘  └─┘                
st   ────────────────────────────────────┘└┘
119      { use [x, 0] }},
id              
src        └───┘ └───┘
typ        └───┘└───┘
doc        └───┘ └───┘
txt        └───┘ └───┘
par        └───┘ └───┘
pid           └┘ └──┘
st   ────────────────┘└─┘
120    choose center radius H using this,
id                                  └──┘
src    └───────────────────────────┘
typ    └───────────────────────────┘└──┘
doc    └───────────────────────────┘
txt    └───────────────────────────┘
par    └───────────────────────────┘
pid          └─────┘└───────┘└─────┘
st   ──────────────────────────────────┘└─
121  
st   
122    refine subset.antisymm (subset_univ _) (λx hx, _),
id            └─────────────┘  └─────────┘
src    └─────┘└─────────────┘ └─────────┘└──┘  └──────┘
typ    └─────┘└─────────────┘ └─────────┘└──┘  └──────┘
doc    └─────┘                           └──┘  └──────┘
txt    └─────┘                           └──┘  └──────┘
par    └─────┘                           └──┘  └──────┘
pid                                     └──┘  └──────┘
st   ──────────────────────────────────────────────────┘└─
123    refine metric.mem_closure_iff'.2 (λε εpos, _),
id            └─────────────────────┘
src    └─────┘└─────────────────────┘└─┘  └────────┘
typ    └─────┘└─────────────────────┘└─┘  └────────┘
doc    └─────┘└─────────────────────┘└─┘  └────────┘
txt    └─────┘                       └─┘  └────────┘
par    └─────┘                       └─┘  └────────┘
pid                                 └─┘  └────────┘
st   ──────────────────────────────────────────────┘└─
124    /- ε is positive. We have to find a point in the ball of radius ε around x belonging to all `f n`.
st   ─────────────────────────────────────────────────────────────────────────────────────────────────────
125    For this, we construct inductively a sequence `F n = (c n, r n)` such that the closed ball
st   ─────────────────────────────────────────────────────────────────────────────────────────────
126    `closed_ball (c n) (r n)` is included in the previous ball and in `f n`, and such that
st   ─────────────────────────────────────────────────────────────────────────────────────────
127    `r n` is small enough to ensure that `c n` is a Cauchy sequence. Then `c n` converges to a
st   ─────────────────────────────────────────────────────────────────────────────────────────────
128    limit which belongs to all the `f n`. -/
st   ───────────────────────────────────────────
129    let F : ℕ → (α × ℝ) := λn, nat.rec_on n (prod.mk x (min (ε/2) 1))
id                              └────────┘              └─┘  
src    └──────┘     └───┘ └─┘└────────┘           └─┘   └──────
typ    └──────┘    └───┘ └─┘└────────┘          └─┘  └──────
doc    └──────┘      └───┘ └─┘                           └──────
txt    └──────┘      └───┘ └─┘                           └──────
par    └──────┘      └───┘ └─┘                           └──────
pid    └───┘└─┘      └──┘ └─┘                           └──────
st   ────────────────────────────────────────────────────────────────────
130                                (λn p, prod.mk (center n p.1 p.2) (radius n p.1 p.2)),
id                                        └─────┘  └────┘             └────┘
src  ─────────────────────────────┘  └───┘└─────┘         └─┘ └──┘         └─┘ └──┘
typ  ─────────────────────────────┘  └───┘└─────┘ └────┘  └─┘ └──┘ └────┘  └─┘ └──┘
doc  ─────────────────────────────┘  └───┘                └─┘ └──┘         └─┘ └──┘
txt  ─────────────────────────────┘  └───┘                └─┘ └──┘         └─┘ └──┘
par  ─────────────────────────────┘  └───┘                └─┘ └──┘         └─┘ └──┘
pid  ─────────────────────────────┘  └───┘                └─┘ └──┘         └─┘ └──┘
st   ──────────────────────────────────────────────────────────────────────────────────┘└─
131    let c : ℕ → α := λn, (F n).1,
id                          
src    └──────┘   └──┘ └─┘   └─┘
typ    └──────┘  └──┘ └─┘  └─┘
doc    └──────┘   └──┘ └─┘   └─┘
txt    └──────┘   └──┘ └─┘   └─┘
par    └──────┘   └──┘ └─┘   └─┘
pid    └───┘└─┘   └──┘ └─┘   └┘
st   ─────────────────────────────┘└─
132    let r : ℕ → ℝ := λn, (F n).2,
id                           
src    └──────┘   └──┘ └─┘   └─┘
typ    └──────┘   └──┘ └─┘  └─┘
doc    └──────┘   └──┘ └─┘   └─┘
txt    └──────┘   └──┘ └─┘   └─┘
par    └──────┘   └──┘ └─┘   └─┘
pid    └───┘└─┘   └──┘ └─┘   └┘
st   ─────────────────────────────┘└─
133    have rpos : ∀n, r n > 0,
id                     
src    └──────────┘     └┘
typ    └──────────┘    └┘
doc    └──────────┘     └┘
txt    └──────────┘     └┘
par    └──────────┘     └┘
pid    └───────┘└─┘     
st   ────────────────────────┘└─
134    { assume n,
src      └──────┘
typ      └──────┘
doc      └──────┘
txt      └──────┘
par      └──────┘
pid      └──────┘
st   ───┘└──────┘└─
135      induction n with n hn,
id                 
src      └────────┘ └────────┘
typ      └────────┘└────────┘
doc      └────────┘ └────────┘
txt      └────────┘ └────────┘
par      └────────┘ └────────┘
pid                └───────┘
st   ────────────────────────┘└─
136      exact lt_min (half_pos εpos) (zero_lt_one),
id             └────┘  └──────┘ └──┘   └─────────┘
src      └────┘└────┘ └──────┘    └┘ └─────────┘
typ      └────┘└────┘ └──────┘└──┘└┘ └─────────┘
doc      └────┘                   └┘            
txt      └────┘                   └┘            
par      └────┘                   └┘            
pid                              └┘            
st   ─────────────────────────────────────────────┘└─
137      exact (H n (c n) (r n) hn).1 },
id                          └┘
src      └────┘      └┘   └┘  └──┘
typ      └────┘    └┘ └┘└┘└──┘
doc      └────┘      └┘   └┘  └──┘
txt      └────┘      └┘   └┘  └──┘
par      └────┘      └┘   └┘  └──┘
pid                 └┘   └┘  └─┘
st   ────────────────────────────────┘└┘
138    have rB : ∀n, r n ≤ B n,
id                        
src    └────────┘      
typ    └────────┘    
doc    └────────┘      
txt    └────────┘      
par    └────────┘      
pid    └─────┘└─┘      
st   ────────────────────────┘└─
139    { assume n,
src      └──────┘
typ      └──────┘
doc      └──────┘
txt      └──────┘
par      └──────┘
pid      └──────┘
st   ───┘└──────┘└─
140      induction n with n hn,
id                 
src      └────────┘ └────────┘
typ      └────────┘└────────┘
doc      └────────┘ └────────┘
txt      └────────┘ └────────┘
par      └────────┘ └────────┘
pid                └───────┘
st   ────────────────────────┘└─
141      exact min_le_right _ _,
id             └──────────┘
src      └────┘└──────────┘└──┘
typ      └────┘└──────────┘└──┘
doc      └────┘            └──┘
txt      └────┘            └──┘
par      └────┘            └──┘
pid                       └──┘
st   ─────────────────────────┘└─
142      exact (H n (c n) (r n) (rpos n)).2.1 },
id                            └──┘ 
src      └────┘      └┘   └┘      └─────┘
typ      └────┘    └┘  └┘ └──┘└─────┘
doc      └────┘      └┘   └┘      └─────┘
txt      └────┘      └┘   └┘      └─────┘
par      └────┘      └┘   └┘      └─────┘
pid                 └┘   └┘      └──┘└─┘
st   ────────────────────────────────────────┘└┘
143    have incl : ∀n, closed_ball (c (n+1)) (r (n+1)) ⊆ (closed_ball (c n) (r n)) ∩ (f n) :=
id                                                        └─────────┘               
src    └──────────┘                  └──┘     └──┘  └─────────┘   └┘   └─┘    └────
typ    └──────────┘                  └──┘     └──┘  └─────────┘  └┘  └─┘   └────
doc    └──────────┘                  └──┘     └──┘  └─────────┘   └┘   └─┘    └────
txt    └──────────┘                  └──┘     └──┘                └┘   └─┘    └────
par    └──────────┘                  └──┘     └──┘                └┘   └─┘    └────
pid    └───────┘└─┘                  └──┘     └──┘                └┘   └─┘    └───
st   ─────────────────────────────────────────────────────────────────────────────────────────
144      λn, (H n (c n) (r n) (rpos n)).2.2,
id                          └──┘
src  ───┘ └─┘      └┘   └┘      └────┘
typ  ───┘ └─┘    └┘  └┘ └──┘ └────┘
doc  ───┘ └─┘      └┘   └┘      └────┘
txt  ───┘ └─┘      └┘   └┘      └────┘
par  ───┘ └─┘      └┘   └┘      └────┘
pid  ───┘ └─┘      └┘   └┘      └──┘└┘
st   ─────────────────────────────────────┘└─
145    have cdist : ∀n, dist (c n) (c (n+1)) ≤ B n,
id                      └──┘                  
src    └───────────┘  └──┘   └┘     └──┘  
typ    └───────────┘  └──┘   └┘    └──┘ 
doc    └───────────┘         └┘     └──┘  
txt    └───────────┘         └┘     └──┘  
par    └───────────┘         └┘     └──┘  
pid    └────────┘└─┘         └┘     └──┘  
st   ────────────────────────────────────────────┘└─
146    { assume n,
src      └──────┘
typ      └──────┘
doc      └──────┘
txt      └──────┘
par      └──────┘
pid      └──────┘
st   ───┘└──────┘└─
147      rw dist_comm,
id          └───────┘
src      └─┘└───────┘
typ      └─┘└───────┘
doc      └─┘
txt      └─┘
par      └─┘
pid        
st   ───────────────┘└─
148      have A : c (n+1) ∈ closed_ball (c (n+1)) (r (n+1)) :=
id                          └─────────┘             
src      └───────┘    └─┘ └─────────┘     └──┘     └──────
typ      └───────┘    └─┘ └─────────┘    └──┘   └──────
doc      └───────┘    └─┘ └─────────┘     └──┘     └──────
txt      └───────┘    └─┘                 └──┘     └──────
par      └───────┘    └─┘                 └──┘     └──────
pid      └────┘└─┘    └─┘                 └──┘     └─┘└───
st   ──────────────────────────────────────────────────────────
149        mem_closed_ball_self (le_of_lt (rpos (n+1))),
id         └──────────────────┘  └──────┘  └──┘  
src  ─────┘└──────────────────┘ └──────┘        └──┘
typ  ─────┘└──────────────────┘ └──────┘ └──┘  └──┘
doc  ─────┘                                     └──┘
txt  ─────┘                                     └──┘
par  ─────┘                                     └──┘
pid  ─────┘                                     └──┘
st   ─────────────────────────────────────────────────┘└─
150      have I := calc
src      └────────┘    
typ      └────────┘    
doc      └────────┘    
txt      └────────┘    
par      └────────┘    
pid      └────┘└─┘    
st   ───────────────────
151        closed_ball (c (n+1)) (r (n+1)) ⊆ closed_ball (c n) (r n) :
id                                                              
src  ─────┘                └──┘     └──┘               └┘   └───
typ  ─────┘                └──┘     └──┘               └┘  └───
doc  ─────┘                └──┘     └──┘               └┘   └───
txt  ─────┘                └──┘     └──┘               └┘   └───
par  ─────┘                └──┘     └──┘               └┘   └───
pid  ─────┘                └──┘     └──┘               └┘   └───
st   ──────────────────────────────────────────────────────────────────
152          subset.trans (incl n) (inter_subset_left _ _)
id           └──────────┘  └──┘     └───────────────┘
src  ───────┘└──────────┘      └┘ └───────────────┘└─────
typ  ───────┘└──────────┘ └──┘ └┘ └───────────────┘└─────
doc  ───────┘                  └┘                  └─────
txt  ───────┘                  └┘                  └─────
par  ───────┘                  └┘                  └─────
pid  ───────┘                  └┘                  └─────
st   ──────────────────────────────────────────────────────
153        ... ⊆ closed_ball (c n) (B n) : closed_ball_subset_closed_ball (rB n),
id               └─────────┘             └────────────────────────────┘  └┘ 
src  ─────────┘ └─────────┘   └┘   └──┘└────────────────────────────┘    
typ  ─────────┘ └─────────┘  └┘  └──┘└────────────────────────────┘ └┘
doc  ─────────┘ └─────────┘   └┘   └──┘                                  
txt  ─────────┘               └┘   └──┘                                  
par  ─────────┘               └┘   └──┘                                  
pid  ─────────┘               └┘   └──┘                                  
st   ──────────────────────────────────────────────────────────────────────────┘└─
154      exact I A },
id              
src      └────┘  
typ      └────┘
doc      └────┘  
txt      └────┘  
par      └────┘  
pid             
st   ─────────────┘└┘
155    have : cauchy_seq c,
id            └────────┘ 
src    └─────┘└────────┘
typ    └─────┘└────────┘
doc    └─────┘└────────┘
txt    └─────┘          
par    └─────┘          
pid    └───┘└┘          
st   ────────────────────┘└─
156    { refine cauchy_seq_of_le_geometric (1/2) 1 (by norm_num) (λn, _),
id              └────────────────────────┘
src      └─────┘└────────────────────────┘  └───┘   └──────┘└┘  └───┘
typ      └─────┘└────────────────────────┘  └───┘   └──────┘└┘  └───┘
doc      └─────┘└────────────────────────┘  └───┘   └──────┘└┘  └───┘
txt      └─────┘                            └───┘   └──────┘└┘  └───┘
par      └─────┘                            └───┘   └──────┘└┘  └───┘
pid                                        └───┘   └─────────┘  └───┘
st   ───┘└───────────────────────────────────────────┘└───────┘└───────┘└─
157      rw one_mul,
id          └─────┘
src      └─┘└─────┘
typ      └─┘└─────┘
doc      └─┘
txt      └─┘
par      └─┘
pid        
st   ─────────────┘└─
158      exact cdist n },
id             └───┘ 
src      └────┘      
typ      └────┘└───┘
doc      └────┘      
txt      └────┘      
par      └────┘      
pid                 
st   ─────────────────┘└┘
159    -- as the sequence `c n` is Cauchy in a complete space, it converges to a limit `y`.
st   ───────────────────────────────────────────────────────────────────────────────────────
160    rcases cauchy_seq_tendsto_of_complete this with ⟨y, ylim⟩,
id            └────────────────────────────┘ └──┘
src    └─────┘└────────────────────────────┘    └─────────────┘
typ    └─────┘└────────────────────────────┘└──┘└─────────────┘
doc    └─────┘└────────────────────────────┘    └─────────────┘
txt    └─────┘                                  └─────────────┘
par    └─────┘                                  └─────────────┘
pid                                            └─────────────┘
st   ──────────────────────────────────────────────────────────┘└─
161    -- this point `y` will be the desired point. We will check that it belongs to all
st   ────────────────────────────────────────────────────────────────────────────────────
162    -- `f n` and to `ball x ε`.
st   ──────────────────────────────
163    use y,
id         
src    └──┘
typ    └──┘
doc    └──┘
txt    └──┘
par    └──┘
pid       
st   ──────┘└─
164    simp only [exists_prop, set.mem_Inter],
id                └─────────┘  └───────────┘
src    └─────────┘└─────────┘└┘└───────────┘
typ    └─────────┘└─────────┘└┘└───────────┘
doc    └─────────┘           └┘             
txt    └─────────┘           └┘             
par    └─────────┘           └┘             
pid        └──┘└┘           └┘             
st   ───────────────────────────────────────┘└─
165    have I : ∀n, ∀m ≥ n, closed_ball (c m) (r m) ⊆ closed_ball (c n) (r n),
id                                                    └─────────┘       
src    └───────┘   └──┘                └┘   └┘ └─────────┘   └┘   
typ    └───────┘   └──┘                └┘   └┘ └─────────┘  └┘  
doc    └───────┘   └──┘                └┘   └┘ └─────────┘   └┘   
txt    └───────┘   └──┘                └┘   └┘               └┘   
par    └───────┘   └──┘                └┘   └┘               └┘   
pid    └────┘└─┘   └──┘                └┘   └┘               └┘   
st   ───────────────────────────────────────────────────────────────────────┘└─
166    { assume n,
src      └──────┘
typ      └──────┘
doc      └──────┘
txt      └──────┘
par      └──────┘
pid      └──────┘
st   ───┘└──────┘└─
167      refine nat.le_induction _ (λm hnm h, _),
id              └──────────────┘
src      └─────┘└──────────────┘└─┘  └─────────┘
typ      └─────┘└──────────────┘└─┘  └─────────┘
doc      └─────┘└──────────────┘└─┘  └─────────┘
txt      └─────┘                └─┘  └─────────┘
par      └─────┘                └─┘  └─────────┘
pid                            └─┘  └─────────┘
st   ──────────────────────────────────────────┘└─
168      { exact subset.refl _ },
id               └─────────┘
src        └────┘└─────────┘└─┘
typ        └────┘└─────────┘└─┘
doc        └────┘           └─┘
txt        └────┘           └─┘
par        └────┘           └─┘
pid                        └┘
st   ─────┘└──────────────────┘└┘
169      { exact subset.trans (incl m) (subset.trans (inter_subset_left _ _) h) }},
id                             └──┘    └──────────┘  └───────────────┘      
src        └────┘                  └┘ └──────────┘ └───────────────┘└────┘ └┘
typ        └────┘             └──┘└┘ └──────────┘ └───────────────┘└────┘└┘
doc        └────┘                  └┘                               └────┘ └┘
txt        └────┘                  └┘                               └────┘ └┘
par        └────┘                  └┘                               └────┘ └┘
pid                               └┘                               └────┘ 
st   ──────────────────────────────────────────────────────────────────────────┘└─┘
170    have yball : ∀n, y ∈ closed_ball (c n) (r n),
id                         └─────────┘       
src    └───────────┘    └─────────┘   └┘   
typ    └───────────┘   └─────────┘  └┘  
doc    └───────────┘    └─────────┘   └┘   
txt    └───────────┘                  └┘   
par    └───────────┘                  └┘   
pid    └────────┘└─┘                  └┘   
st   ─────────────────────────────────────────────┘└─
171    { assume n,
src      └──────┘
typ      └──────┘
doc      └──────┘
txt      └──────┘
par      └──────┘
pid      └──────┘
st   ───┘└──────┘└─
172      refine mem_of_closed_of_tendsto (by simp) ylim is_closed_ball _,
id              └──────────────────────┘           └──┘ └────────────┘
src      └─────┘└──────────────────────┘   └──┘└┘    └────────────┘└┘
typ      └─────┘└──────────────────────┘   └──┘└┘└──┘└────────────┘└┘
doc      └─────┘                           └──┘└┘                  └┘
txt      └─────┘                           └──┘└┘                  └┘
par      └─────┘                           └──┘└┘                  └┘
pid                                       └─────┘                  └┘
st   ──────────────────────────────────────┘└───┘└─────────────────────┘└─
173      simp only [filter.mem_at_top_sets, nonempty_of_inhabited, set.mem_preimage],
id                  └────────────────────┘  └───────────────────┘  └──────────────┘
src      └─────────┘└────────────────────┘└┘└───────────────────┘└┘└──────────────┘
typ      └─────────┘└────────────────────┘└┘└───────────────────┘└┘└──────────────┘
doc      └─────────┘                      └┘                     └┘                
txt      └─────────┘                      └┘                     └┘                
par      └─────────┘                      └┘                     └┘                
pid          └──┘└┘                      └┘                     └┘                
st   ──────────────────────────────────────────────────────────────────────────────┘└─
174      exact ⟨n, λm hm, I n m hm (mem_closed_ball_self (le_of_lt (rpos m)))⟩ },
id                                └──────────────────┘  └──────┘  └──┘
src      └────┘  └┘ └────┘      └──────────────────┘ └──────┘      └───┘
typ      └────┘  └┘ └────┘    └──────────────────┘ └──────┘ └──┘ └───┘
doc      └────┘  └┘ └────┘                                         └───┘
txt      └────┘  └┘ └────┘                                         └───┘
par      └────┘  └┘ └────┘                                         └───┘
pid             └┘ └────┘                                         └──┘
st   ─────────────────────────────────────────────────────────────────────────┘└┘
175    split,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
st   ──────┘└─
176    show ∀n, y ∈ f n,
id                 
src    └───┘     
typ    └───┘   
doc    └───┘     
txt    └───┘     
par    └───┘     
pid    └───┘     
st   ────────────────────
177    { assume n,
src      └──────┘
typ      └──────┘
doc      └──────┘
txt      └──────┘
par      └──────┘
pid      └──────┘
st   ───┘└──────┘└─
178      have : closed_ball (c (n+1)) (r (n+1)) ⊆ f n := subset.trans (incl n) (inter_subset_right _ _),
id              └─────────┘                          └──────────┘  └──┘    └────────────────┘
src      └─────┘└─────────┘     └──┘     └──┘   └──┘└──────────┘      └┘ └────────────────┘└───┘
typ      └─────┘└─────────┘    └──┘    └──┘ └──┘└──────────┘ └──┘└┘ └────────────────┘└───┘
doc      └─────┘└─────────┘     └──┘     └──┘   └──┘                  └┘                   └───┘
txt      └─────┘                └──┘     └──┘   └──┘                  └┘                   └───┘
par      └─────┘                └──┘     └──┘   └──┘                  └┘                   └───┘
pid      └───┘└┘                └──┘     └──┘   └──┘                  └┘                   └───┘
st   ─────────────────────────────────────────────────────────────────────────────────────────────────┘└─
179      exact this (yball (n+1)) },
id             └──┘  └───┘  
src      └────┘             └──┘
typ      └────┘└──┘ └───┘  └──┘
doc      └────┘             └──┘
txt      └────┘             └──┘
par      └────┘             └──┘
pid                        └─┘
st   ────────────────────────────┘└┘
180    show dist x y < ε, from calc
id          └──┘     
src    └───┘└──┘      └───┘    
typ    └───┘└──┘   └───┘    
doc    └───┘          └───┘    
txt    └───┘          └───┘    
par    └───┘          └───┘    
pid    └───┘          └───┘    
st   ───────────────────────────────
181      dist x y = dist y x : dist_comm _ _
id                  └──┘     └───────┘
src  ───┘       └──┘  └─┘└───────┘└────
typ  ───┘       └──┘└─┘└───────┘└────
doc  ───┘             └─┘         └────
txt  ───┘             └─┘         └────
par  ───┘             └─┘         └────
pid  ───┘             └─┘         └────
st   ────────────────────────────────────────
182      ... ≤ r 0 : yball 0
id                  └───┘
src  ───────┘  └───┘     └──
typ  ───────┘ └───┘└───┘└──
doc  ───────┘  └───┘     └──
txt  ───────┘  └───┘     └──
par  ───────┘  └───┘     └──
pid  ───────┘  └───┘     └──
st   ────────────────────────
183      ... < ε : lt_of_le_of_lt (min_le_left _ _) (half_lt_self εpos)
id                └────────────┘  └─────────┘       └──────────┘ └──┘
src  ───────┘  └─┘└────────────┘ └─────────┘└────┘ └──────────┘    └┘
typ  ───────┘ └─┘└────────────┘ └─────────┘└────┘ └──────────┘└──┘└┘
doc  ───────┘  └─┘                          └────┘                 └┘
txt  ───────┘  └─┘                          └────┘                 └┘
par  ───────┘  └─┘                          └────┘                 └┘
pid  ───────┘  └─┘                          └────┘                 
st   ──────────────────────────────────────────────────────────────────┘
184  end
st   └─┘
185  
186  /-- Baire theorem: a countable intersection of dense open sets is dense. Formulated here with ⋂₀. -/
187  theorem dense_sInter_of_open {S : set (set α)} (ho : ∀s∈S, is_open s) (hS : countable S)
id                                     └─┘  └─┘              └─────┘         └───────┘ 
src                                    └─┘  └─┘                 └─────┘          └───────┘
typ                                    └─┘  └─┘              └─────┘         └───────┘ 
doc                                                             └─────┘          └───────┘
188    (hd : ∀s∈S, closure s = univ) : closure (⋂₀S) = univ :=
id               └─────┘   └──┘    └─────┘  └┘   └──┘
src                └─────┘    └──┘    └─────┘  └┘    └──┘
typ              └─────┘   └──┘    └─────┘  └┘   └──┘
doc                └─────┘             └─────┘  └┘
189  begin
st   └─────
190    cases S.eq_empty_or_nonempty with h h,
id           └────────────────────┘
src    └────┘└────────────────────┘└───────┘
typ    └────┘└────────────────────┘└───────┘
doc    └────┘                      └───────┘
txt    └────┘                      └───────┘
par    └────┘                      └───────┘
pid                               └───────┘
st   ──────────────────────────────────────┘└─
191    { simp [h] },
id             
src      └────┘ └┘
typ      └────┘└┘
doc      └────┘ └┘
txt      └────┘ └┘
par      └────┘ └┘
pid           
st   ───┘└───────┘└┘
192    { rcases exists_surjective_of_countable h hS with ⟨f, hf⟩,
id              └────────────────────────────┘  └┘
src      └─────┘└────────────────────────────┘   └───────────┘
typ      └─────┘└────────────────────────────┘└┘└───────────┘
doc      └─────┘                                 └───────────┘
txt      └─────┘                                 └───────────┘
par      └─────┘                                 └───────────┘
pid                                             └───────────┘
st   ──────────────────────────────────────────────────────────┘└─
193      have F : ∀n, f n ∈ S := λn, by rw hf; exact mem_range_self _,
id                                      └┘        └────────────┘
src      └───────┘     └──┘ └─┘  └─┘  └┘└────┘└────────────┘└┘
typ      └───────┘   └──┘ └─┘  └─┘└┘└┘└────┘└────────────┘└┘
doc      └───────┘      └──┘ └─┘  └─┘  └┘└────┘              └┘
txt      └───────┘      └──┘ └─┘  └─┘  └┘└────┘              └┘
par      └───────┘      └──┘ └─┘  └─┘  └┘└────┘              └┘
pid      └────┘└─┘      └──┘ └─┘  └──┘  └──────┘              └┘
st   ─────────────────────────────────┘└────────────────────────────┘└─
194      rw [hf, sInter_range],
id           └┘  └──────────┘
src      └──┘  └┘└──────────┘
typ      └──┘└┘└┘└──────────┘
doc      └──┘  └┘            
txt      └──┘  └┘            
par      └──┘  └┘            
pid        └┘  └┘            
st   ─────────┘└────────────┘└──
195      exact dense_Inter_of_open_nat (λn, ho _ (F n)) (λn, hd _ (F n)) }
id             └─────────────────────┘      └┘               └┘    
src      └────┘└─────────────────────┘  └─┘  └─┘   └─┘  └─┘  └─┘   └─┘
typ      └────┘└─────────────────────┘  └─┘└┘└─┘   └─┘  └─┘└┘└─┘  └─┘
doc      └────┘└─────────────────────┘  └─┘  └─┘   └─┘  └─┘  └─┘   └─┘
txt      └────┘                         └─┘  └─┘   └─┘  └─┘  └─┘   └─┘
par      └────┘                         └─┘  └─┘   └─┘  └─┘  └─┘   └─┘
pid                                    └─┘  └─┘   └─┘  └─┘  └─┘   └┘
st   ───────────────────────────────────────────────────────────────────┘└─
196  end
st   ──┘
197  
198  /-- Baire theorem: a countable intersection of dense open sets is dense. Formulated here with
199  an index set which is a countable set in any type. -/
200  theorem dense_bInter_of_open {S : set β} {f : β → set α} (ho : ∀s∈S, is_open (f s))
id                                     └─┘           └─┘             └─────┘   
src                                    └─┘             └─┘                └─────┘
typ                                    └─┘           └─┘             └─────┘   
doc                                                                       └─────┘
201    (hS : countable S) (hd : ∀s∈S, closure (f s) = univ) : closure (⋂s∈S, f s) = univ :=
id           └───────┘             └─────┘      └──┘    └─────┘        └──┘
src          └───────┘                └─────┘        └──┘    └─────┘            └──┘
typ          └───────┘             └─────┘      └──┘    └─────┘        └──┘
doc          └───────┘                └─────┘                 └─────┘     
202  begin
st   └─────
203    rw ← sInter_image,
id          └──────────┘
src    └───┘└──────────┘
typ    └───┘└──────────┘
doc    └───┘
txt    └───┘
par    └───┘
pid      └─┘
st   ──────────────────┘└─
204    apply dense_sInter_of_open,
id           └──────────────────┘
src    └────┘└──────────────────┘
typ    └────┘└──────────────────┘
doc    └────┘└──────────────────┘
txt    └────┘
par    └────┘
pid         
st   ───────────────────────────┘└─
205    { rwa ball_image_iff },
id           └────────────┘
src      └──┘└────────────┘
typ      └──┘└────────────┘
doc      └──┘              
txt      └──┘              
par      └──┘              
pid                       
st   ───┘└─────────────────┘└┘
206    { exact countable_image _ hS },
id             └─────────────┘   └┘
src      └────┘└─────────────┘└─┘  
typ      └────┘└─────────────┘└─┘└┘
doc      └────┘               └─┘  
txt      └────┘               └─┘  
par      └────┘               └─┘  
pid                          └─┘  
st   ───┘└─────────────────────────┘└┘
207    { rwa ball_image_iff }
id           └────────────┘
src      └──┘└────────────┘
typ      └──┘└────────────┘
doc      └──┘              
txt      └──┘              
par      └──┘              
pid                       
st   ──────────────────────┘└─
208  end
st   ──┘
209  
210  /-- Baire theorem: a countable intersection of dense open sets is dense. Formulated here with
211  an index set which is an encodable type. -/
212  theorem dense_Inter_of_open [encodable β] {f : β → set α} (ho : ∀s, is_open (f s))
id                                └───────┘           └─┘            └─────┘   
src                               └───────┘             └─┘              └─────┘
typ                               └───────┘           └─┘            └─────┘   
doc                               └───────┘                              └─────┘
213    (hd : ∀s, closure (f s) = univ) : closure (⋂s, f s) = univ :=
id              └─────┘      └──┘    └─────┘       └──┘
src              └─────┘        └──┘    └─────┘          └──┘
typ             └─────┘      └──┘    └─────┘       └──┘
doc              └─────┘                 └─────┘   
214  begin
st   └─────
215    rw ← sInter_range,
id          └──────────┘
src    └───┘└──────────┘
typ    └───┘└──────────┘
doc    └───┘
txt    └───┘
par    └───┘
pid      └─┘
st   ──────────────────┘└─
216    apply dense_sInter_of_open,
id           └──────────────────┘
src    └────┘└──────────────────┘
typ    └────┘└──────────────────┘
doc    └────┘└──────────────────┘
txt    └────┘
par    └────┘
pid         
st   ───────────────────────────┘└─
217    { rwa forall_range_iff },
id           └──────────────┘
src      └──┘└──────────────┘
typ      └──┘└──────────────┘
doc      └──┘                
txt      └──┘                
par      └──┘                
pid                         
st   ───┘└───────────────────┘└┘
218    { exact countable_range _ },
id             └─────────────┘
src      └────┘└─────────────┘└─┘
typ      └────┘└─────────────┘└─┘
doc      └────┘               └─┘
txt      └────┘               └─┘
par      └────┘               └─┘
pid                          └┘
st   ───┘└──────────────────────┘└┘
219    { rwa forall_range_iff }
id           └──────────────┘
src      └──┘└──────────────┘
typ      └──┘└──────────────┘
doc      └──┘                
txt      └──┘                
par      └──┘                
pid                         
st   ────────────────────────┘└─
220  end
st   ──┘
221  
222  /-- Baire theorem: a countable intersection of dense Gδ sets is dense. Formulated here with ⋂₀. -/
223  theorem dense_sInter_of_Gδ {S : set (set α)} (ho : ∀s∈S, is_Gδ s) (hS : countable S)
id                                   └─┘  └─┘              └───┘         └───────┘ 
src                                  └─┘  └─┘                 └───┘          └───────┘
typ                                  └─┘  └─┘              └───┘         └───────┘ 
doc                                                           └───┘          └───────┘
224    (hd : ∀s∈S, closure s = univ) : closure (⋂₀S) = univ :=
id               └─────┘   └──┘    └─────┘  └┘   └──┘
src                └─────┘    └──┘    └─────┘  └┘    └──┘
typ              └─────┘   └──┘    └─────┘  └┘   └──┘
doc                └─────┘             └─────┘  └┘
225  begin
st   └─────
226    -- the result follows from the result for a countable intersection of dense open sets,
st   ─────────────────────────────────────────────────────────────────────────────────────────
227    -- by rewriting each set as a countable intersection of open sets, which are of course dense.
st   ────────────────────────────────────────────────────────────────────────────────────────────────
228    have : ∀s : set α, ∃T : set (set α), s ∈ S → ((∀t ∈ T, is_open t) ∧ countable T ∧ s = (⋂₀ T)),
id                 └─┘        └─┘  └─┘                   └─────┘     └───────┘         └┘
src    └─────┘ └──┘     └──┘    └─┘        └──┘  └─────┘ └┘└───────┘    └┘ └┘
typ    └─────┘ └──┘└─┘  └──┘└─┘ └─┘     └──┘  └─────┘ └┘└───────┘    └┘ └┘
doc    └─────┘ └──┘      └──┘                └──┘  └─────┘ └┘ └───────┘     └┘ └┘
txt    └─────┘ └──┘      └──┘                └──┘          └┘                  └┘
par    └─────┘ └──┘      └──┘                └──┘          └┘                  └┘
pid    └───┘└┘ └──┘      └──┘                └──┘          └┘                  └┘
st   ──────────────────────────────────────────────────────────────────────────────────────────────┘└─
229    { assume s,
src      └──────┘
typ      └──────┘
doc      └──────┘
txt      └──────┘
par      └──────┘
pid      └──────┘
st   ───┘└──────┘└─
230      by_cases hs : s ∈ S,
id                        
src      └───────┘  └─┘  
typ      └───────┘  └─┘ 
doc      └───────┘  └─┘  
txt      └───────┘  └─┘  
par      └───────┘  └─┘  
pid                └─┘  
st   ──────────────────────┘└─
231      { simp [hs], exact ho s hs },
id               └┘         └┘  └┘
src        └────┘    └────┘     
typ        └────┘└┘  └────┘└┘└┘
doc        └────┘    └────┘     
txt        └────┘    └────┘     
par        └────┘    └────┘     
pid                          
st   ─────┘└───────┘└──────────────┘└┘
232      { simp [hs] }},
id               └┘
src        └────┘  └┘
typ        └────┘└┘└┘
doc        └────┘  └┘
txt        └────┘  └┘
par        └────┘  └┘
pid              
st   ───────────────┘└─┘
233    choose T hT using this,
id                       └──┘
src    └────────────────┘
typ    └────────────────┘└──┘
doc    └────────────────┘
txt    └────────────────┘
par    └────────────────┘
pid          └┘└─┘└─────┘
st   ───────────────────────┘└─
234    have : ⋂₀ S = ⋂₀ (⋃s∈S, T s) := (sInter_bUnion (λs hs, (hT s hs).2.2)).symm,
id                                  └───────────┘          └┘
src    └─────┘       └┘   └───┘ └───────────┘  └────┘      └──────────┘
typ    └─────┘       └┘ └───┘ └───────────┘  └────┘ └┘   └──────────┘
doc    └─────┘       └┘   └───┘                └────┘      └──────────┘
txt    └─────┘        └┘    └───┘                └────┘      └──────────┘
par    └─────┘        └┘    └───┘                └────┘      └──────────┘
pid    └───┘└┘        └┘    └──┘                └────┘      └─────────┘
st   ────────────────────────────────────────────────────────────────────────────┘└─
235    rw this,
id        └──┘
src    └─┘
typ    └─┘└──┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ────────┘└─
236    refine dense_sInter_of_open (λt ht, _) (countable_bUnion hS (λs hs, (hT s hs).2.1)) (λt ht, _),
id            └──────────────────┘             └──────────────┘ └┘          └┘
src    └─────┘└──────────────────┘  └───────┘ └──────────────┘    └────┘      └──────┘  └──────┘
typ    └─────┘└──────────────────┘  └───────┘ └──────────────┘└┘  └────┘ └┘   └──────┘  └──────┘
doc    └─────┘└──────────────────┘  └───────┘                     └────┘      └──────┘  └──────┘
txt    └─────┘                      └───────┘                     └────┘      └──────┘  └──────┘
par    └─────┘                      └───────┘                     └────┘      └──────┘  └──────┘
pid                                └───────┘                     └────┘      └──────┘  └──────┘
st   ───────────────────────────────────────────────────────────────────────────────────────────────┘└─
237    show is_open t,
id          └─────┘ 
src    └───┘└─────┘
typ    └───┘└─────┘
doc    └───┘└─────┘
txt    └───┘       
par    └───┘       
pid    └───┘       
st   ──────────────────
238    { simp only [exists_prop, set.mem_Union] at ht,
id                  └─────────┘  └───────────┘
src      └─────────┘└─────────┘└┘└───────────┘└─────┘
typ      └─────────┘└─────────┘└┘└───────────┘└─────┘
doc      └─────────┘           └┘             └─────┘
txt      └─────────┘           └┘             └─────┘
par      └─────────┘           └┘             └─────┘
pid          └──┘└┘           └┘             └───┘
st   ───┘└──────────────────────────────────────────┘└─
239      rcases ht with ⟨s, hs, tTs⟩,
id              └┘
src      └─────┘  └────────────────┘
typ      └─────┘└┘└────────────────┘
doc      └─────┘  └────────────────┘
txt      └─────┘  └────────────────┘
par      └─────┘  └────────────────┘
pid              └────────────────┘
st   ──────────────────────────────┘└─
240      exact (hT s hs).1 t tTs },
id              └┘  └┘     └─┘
src      └────┘      └──┘    
typ      └────┘ └┘└┘└──┘└─┘
doc      └────┘      └──┘    
txt      └────┘      └──┘    
par      └────┘      └──┘    
pid                 └──┘    
st   ───────────────────────────┘└┘
241    show closure t = univ,
id          └─────┘    └──┘
src    └───┘└─────┘  └──┘
typ    └───┘└─────┘ └──┘
doc    └───┘└─────┘  
txt    └───┘         
par    └───┘         
pid    └───┘         
st   ─────────────────────────
242    { simp only [exists_prop, set.mem_Union] at ht,
id                  └─────────┘  └───────────┘
src      └─────────┘└─────────┘└┘└───────────┘└─────┘
typ      └─────────┘└─────────┘└┘└───────────┘└─────┘
doc      └─────────┘           └┘             └─────┘
txt      └─────────┘           └┘             └─────┘
par      └─────────┘           └┘             └─────┘
pid          └──┘└┘           └┘             └───┘
st   ───────────────────────────────────────────────┘└─
243      rcases ht with ⟨s, hs, tTs⟩,
id              └┘
src      └─────┘  └────────────────┘
typ      └─────┘└┘└────────────────┘
doc      └─────┘  └────────────────┘
txt      └─────┘  └────────────────┘
par      └─────┘  └────────────────┘
pid              └────────────────┘
st   ──────────────────────────────┘└─
244      apply subset.antisymm (subset_univ _),
id             └─────────────┘  └─────────┘
src      └────┘└─────────────┘ └─────────┘└─┘
typ      └────┘└─────────────┘ └─────────┘└─┘
doc      └────┘                           └─┘
txt      └────┘                           └─┘
par      └────┘                           └─┘
pid                                      └─┘
st   ────────────────────────────────────────┘└─
245      rw ← (hd s hs),
id             └┘  └┘
src      └───┘      
typ      └───┘ └┘└┘
doc      └───┘      
txt      └───┘      
par      └───┘      
pid        └─┘      
st   ─────────────────┘└─
246      apply closure_mono,
id             └──────────┘
src      └────┘└──────────┘
typ      └────┘└──────────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ─────────────────────┘└─
247      have := sInter_subset_of_mem tTs,
id               └──────────────────┘ └─┘
src      └──────┘└──────────────────┘
typ      └──────┘└──────────────────┘└─┘
doc      └──────┘                    
txt      └──────┘                    
par      └──────┘                    
pid      └───┘└─┘                    
st   ───────────────────────────────────┘└─
248      rwa ← (hT s hs).2.2 at this }
id              └┘  └┘
src      └────┘      └────────────┘
typ      └────┘ └┘└┘└────────────┘
doc      └────┘      └────────────┘
txt      └────┘      └────────────┘
par      └────┘      └────────────┘
pid         └─┘      └─┘└────────┘
st   ───────────────────────────────┘└─
249  end
st   ──┘
250  
251  /-- Baire theorem: a countable intersection of dense Gδ sets is dense. Formulated here with
252  an index set which is a countable set in any type. -/
253  theorem dense_bInter_of_Gδ {S : set β} {f : β → set α} (ho : ∀s∈S, is_Gδ (f s))
id                                   └─┘           └─┘             └───┘   
src                                  └─┘             └─┘                └───┘
typ                                  └─┘           └─┘             └───┘   
doc                                                                     └───┘
254    (hS : countable S) (hd : ∀s∈S, closure (f s) = univ) : closure (⋂s∈S, f s) = univ :=
id           └───────┘             └─────┘      └──┘    └─────┘        └──┘
src          └───────┘                └─────┘        └──┘    └─────┘            └──┘
typ          └───────┘             └─────┘      └──┘    └─────┘        └──┘
doc          └───────┘                └─────┘                 └─────┘     
255  begin
st   └─────
256    rw ← sInter_image,
id          └──────────┘
src    └───┘└──────────┘
typ    └───┘└──────────┘
doc    └───┘
txt    └───┘
par    └───┘
pid      └─┘
st   ──────────────────┘└─
257    apply dense_sInter_of_Gδ,
id           └────────────────┘
src    └────┘└────────────────┘
typ    └────┘└────────────────┘
doc    └────┘└────────────────┘
txt    └────┘
par    └────┘
pid         
st   ─────────────────────────┘└─
258    { rwa ball_image_iff },
id           └────────────┘
src      └──┘└────────────┘
typ      └──┘└────────────┘
doc      └──┘              
txt      └──┘              
par      └──┘              
pid                       
st   ───┘└─────────────────┘└┘
259    { exact countable_image _ hS },
id             └─────────────┘   └┘
src      └────┘└─────────────┘└─┘  
typ      └────┘└─────────────┘└─┘└┘
doc      └────┘               └─┘  
txt      └────┘               └─┘  
par      └────┘               └─┘  
pid                          └─┘  
st   ───┘└─────────────────────────┘└┘
260    { rwa ball_image_iff }
id           └────────────┘
src      └──┘└────────────┘
typ      └──┘└────────────┘
doc      └──┘              
txt      └──┘              
par      └──┘              
pid                       
st   ──────────────────────┘└─
261  end
st   ──┘
262  
263  /-- Baire theorem: a countable intersection of dense Gδ sets is dense. Formulated here with
264  an index set which is an encodable type. -/
265  theorem dense_Inter_of_Gδ [encodable β] {f : β → set α} (ho : ∀s, is_Gδ (f s))
id                              └───────┘           └─┘            └───┘   
src                             └───────┘             └─┘              └───┘
typ                             └───────┘           └─┘            └───┘   
doc                             └───────┘                              └───┘
266    (hd : ∀s, closure (f s) = univ) : closure (⋂s, f s) = univ :=
id              └─────┘      └──┘    └─────┘       └──┘
src              └─────┘        └──┘    └─────┘          └──┘
typ             └─────┘      └──┘    └─────┘       └──┘
doc              └─────┘                 └─────┘   
267  begin
st   └─────
268    rw ← sInter_range,
id          └──────────┘
src    └───┘└──────────┘
typ    └───┘└──────────┘
doc    └───┘
txt    └───┘
par    └───┘
pid      └─┘
st   ──────────────────┘└─
269    apply dense_sInter_of_Gδ,
id           └────────────────┘
src    └────┘└────────────────┘
typ    └────┘└────────────────┘
doc    └────┘└────────────────┘
txt    └────┘
par    └────┘
pid         
st   ─────────────────────────┘└─
270    { rwa forall_range_iff },
id           └──────────────┘
src      └──┘└──────────────┘
typ      └──┘└──────────────┘
doc      └──┘                
txt      └──┘                
par      └──┘                
pid                         
st   ───┘└───────────────────┘└┘
271    { exact countable_range _ },
id             └─────────────┘
src      └────┘└─────────────┘└─┘
typ      └────┘└─────────────┘└─┘
doc      └────┘               └─┘
txt      └────┘               └─┘
par      └────┘               └─┘
pid                          └┘
st   ───┘└──────────────────────┘└┘
272    { rwa forall_range_iff }
id           └──────────────┘
src      └──┘└──────────────┘
typ      └──┘└──────────────┘
doc      └──┘                
txt      └──┘                
par      └──┘                
pid                         
st   ────────────────────────┘└─
273  end
st   ──┘
274  
275  /-- Baire theorem: if countably many closed sets cover the whole space, then their interiors
276  are dense. Formulated here with an index set which is a countable set in any type. -/
277  theorem dense_bUnion_interior_of_closed {S : set β} {f : β → set α} (hc : ∀s∈S, is_closed (f s))
id                                                └─┘           └─┘             └───────┘   
src                                               └─┘             └─┘                └───────┘
typ                                               └─┘           └─┘             └───────┘   
doc                                                                                  └───────┘
278    (hS : countable S) (hU : (⋃s∈S, f s) = univ) : closure (⋃s∈S, interior (f s)) = univ :=
id           └───────┘                └──┘    └─────┘    └──────┘       └──┘
src          └───────┘                     └──┘    └─────┘      └──────┘         └──┘
typ          └───────┘                └──┘    └─────┘    └──────┘       └──┘
doc          └───────┘                              └─────┘      └──────┘
279  begin
st   └─────
280    let g := λs, - (frontier (f s)),
id                    └──────┘  
src    └───────┘ └─┘ └──────┘   └┘
typ    └───────┘ └─┘ └──────┘  └┘
doc    └───────┘ └─┘  └──────┘   └┘
txt    └───────┘ └─┘             └┘
par    └───────┘ └─┘             └┘
pid    └───┘└─┘ └─┘             └┘
st   ────────────────────────────────┘└─
281    have clos_g : closure (⋂s∈S, g s) = univ,
id                   └─────┘          └──┘
src    └────────────┘└─────┘ └┘   └┘└──┘
typ    └────────────┘└─────┘ └┘ └┘└──┘
doc    └────────────┘└─────┘ └┘   └┘ 
txt    └────────────┘         └┘    └┘ 
par    └────────────┘         └┘    └┘ 
pid    └─────────┘└─┘         └┘    └┘ 
st   ─────────────────────────────────────────┘└─
282    { refine dense_bInter_of_open (λs hs, _) hS (λs hs, _),
id              └──────────────────┘            └┘
src      └─────┘└──────────────────┘  └───────┘    └──────┘
typ      └─────┘└──────────────────┘  └───────┘└┘  └──────┘
doc      └─────┘└──────────────────┘  └───────┘    └──────┘
txt      └─────┘                      └───────┘    └──────┘
par      └─────┘                      └───────┘    └──────┘
pid                                  └───────┘    └──────┘
st   ───┘└──────────────────────────────────────────────────┘└─
283      show is_open (g s), from is_open_compl_iff.2 is_closed_frontier,
id            └─────┘           └───────────────┘   └────────────────┘
src      └───┘└─────┘     └───┘└───────────────┘└─┘└────────────────┘
typ      └───┘└─────┘   └───┘└───────────────┘└─┘└────────────────┘
doc      └───┘└─────┘     └───┘                 └─┘└────────────────┘
txt      └───┘            └───┘                 └─┘
par      └───┘            └───┘                 └─┘
pid      └───┘            └───┘                 └─┘
st   ──────────────────────────────────────────────────────────────────┘└─
284      show closure (g s) = univ,
id            └─────┘       └──┘
src      └───┘└─────┘   └┘ └──┘
typ      └───┘└─────┘ └┘ └──┘
doc      └───┘└─────┘   └┘ 
txt      └───┘          └┘ 
par      └───┘          └┘ 
pid      └───┘          └┘ 
st   ───────────────────────────────
285      { apply subset.antisymm (subset_univ _),
id               └─────────────┘  └─────────┘
src        └────┘└─────────────┘ └─────────┘└─┘
typ        └────┘└─────────────┘ └─────────┘└─┘
doc        └────┘                           └─┘
txt        └────┘                           └─┘
par        └────┘                           └─┘
pid                                        └─┘
st   ──────────────────────────────────────────┘└─
286       simp [g, interior_frontier (hc s hs)] }},
id                └───────────────┘  └┘  └┘
src       └────┘ └┘└───────────────┘      └─┘
typ       └────┘└┘└───────────────┘ └┘└┘└─┘
doc       └────┘ └┘└───────────────┘      └─┘
txt       └────┘ └┘                       └─┘
par       └────┘ └┘                       └─┘
pid            └┘                       └┘
st   ──────────────────────────────────────────┘└─┘
287    have : (⋂s∈S, g s) ⊆ (⋃s∈S, interior (f s)),
id                          └──────┘  
src    └─────┘ └┘   └┘ └┘ └──────┘   └┘
typ    └─────┘ └┘  └┘ └┘└──────┘  └┘
doc    └─────┘ └┘   └┘  └┘ └──────┘   └┘
txt    └─────┘  └┘    └┘   └┘             └┘
par    └─────┘  └┘    └┘   └┘             └┘
pid    └───┘└┘  └┘    └┘   └┘             └┘
st   ────────────────────────────────────────────┘└─
288    { assume x hx,
src      └─────────┘
typ      └─────────┘
doc      └─────────┘
txt      └─────────┘
par      └─────────┘
pid      └─────────┘
st   ───┘└─────────┘└─
289      have : x ∈ ⋃s∈S, f s, { have := mem_univ x, rwa ← hU at this },
id                                  └──────┘         └┘
src      └─────┘  └┘       └──────┘└──────┘   └────┘  └───────┘
typ      └─────┘ └┘     └──────┘└──────┘  └────┘└┘└───────┘
doc      └─────┘  └┘       └──────┘           └────┘  └───────┘
txt      └─────┘   └┘        └──────┘           └────┘  └───────┘
par      └─────┘   └┘        └──────┘           └────┘  └───────┘
pid      └───┘└┘   └┘        └───┘└─┘              └─┘  └──────┘
st   ───────────────────────┘└──┘└────────────────┘└─────────────────┘└┘
290      rcases mem_bUnion_iff.1 this with ⟨s, hs, xs⟩,
id              └────────────┘   └──┘
src      └─────┘└────────────┘└─┘    └───────────────┘
typ      └─────┘└────────────┘└─┘└──┘└───────────────┘
doc      └─────┘              └─┘    └───────────────┘
txt      └─────┘              └─┘    └───────────────┘
par      └─────┘              └─┘    └───────────────┘
pid                          └─┘    └───────────────┘
st   ────────────────────────────────────────────────┘└─
291      have : x ∈ g s := mem_bInter_iff.1 hx s hs,
id                      └────────────┘   └┘  └┘
src      └─────┘    └──┘└────────────┘└─┘   
typ      └─────┘ └──┘└────────────┘└─┘└┘└┘
doc      └─────┘    └──┘              └─┘   
txt      └─────┘    └──┘              └─┘   
par      └─────┘    └──┘              └─┘   
pid      └───┘└┘    └──┘              └─┘   
st   ─────────────────────────────────────────────┘└─
292      have : x ∈ interior (f s),
id                 └──────┘   
src      └─────┘  └──────┘   
typ      └─────┘ └──────┘ 
doc      └─────┘  └──────┘   
txt      └─────┘             
par      └─────┘             
pid      └───┘└┘             
st   ────────────────────────────┘└─
293      { have : x ∈ f s \ (frontier (f s)) := mem_inter xs this,
id                         └──────┘         └───────┘ └┘ └──┘
src        └─────┘     └──────┘   └────┘└───────┘  
typ        └─────┘    └──────┘ └────┘└───────┘└┘└──┘
doc        └─────┘      └──────┘   └────┘           
txt        └─────┘                 └────┘           
par        └─────┘                 └────┘           
pid        └───┘└┘                 └┘└──┘           
st   ─────┘└────────────────────────────────────────────────────┘└─
294        simpa [frontier, xs, closure_eq_of_is_closed (hc s hs)] using this },
id                └──────┘  └┘  └─────────────────────┘  └┘  └┘         └──┘
src        └─────┘└──────┘└┘  └┘└─────────────────────┘      └───────┘    
typ        └─────┘└──────┘└┘└┘└┘└─────────────────────┘ └┘└┘└───────┘└──┘
doc        └─────┘└──────┘└┘  └┘                             └───────┘    
txt        └─────┘        └┘  └┘                             └───────┘    
par        └─────┘        └┘  └┘                             └───────┘    
pid                     └┘  └┘                             └┘└────┘    
st   ────────────────────────────────────────────────────────────────────────┘└┘
295      exact mem_bUnion_iff.2 ⟨s, ⟨hs, this⟩⟩ },
id             └────────────┘       └┘  └──┘
src      └────┘└────────────┘└─┘  └┘   └┘    └─┘
typ      └────┘└────────────┘└─┘ └┘ └┘└┘└──┘└─┘
doc      └────┘              └─┘  └┘   └┘    └─┘
txt      └────┘              └─┘  └┘   └┘    └─┘
par      └────┘              └─┘  └┘   └┘    └─┘
pid                         └─┘  └┘   └┘    └┘
st   ──────────────────────────────────────────┘└┘
296    have := closure_mono this,
id             └──────────┘ └──┘
src    └──────┘└──────────┘
typ    └──────┘└──────────┘└──┘
doc    └──────┘            
txt    └──────┘            
par    └──────┘            
pid    └───┘└─┘            
st   ──────────────────────────┘└─
297    rw clos_g at this,
id        └────┘
src    └─┘      └──────┘
typ    └─┘└────┘└──────┘
doc    └─┘      └──────┘
txt    └─┘      └──────┘
par    └─┘      └──────┘
pid            └──────┘
st   ──────────────────┘└─
298    exact subset.antisymm (subset_univ _) this
id           └─────────────┘  └─────────┘    └──┘
src    └────┘└─────────────┘ └─────────┘└──┘    
typ    └────┘└─────────────┘ └─────────┘└──┘└──┘
doc    └────┘                           └──┘    
txt    └────┘                           └──┘    
par    └────┘                           └──┘    
pid                                    └──┘    
st   ────────────────────────────────────────────┘
299  end
st   └─┘
300  
301  /-- Baire theorem: if countably many closed sets cover the whole space, then their interiors
302  are dense. Formulated here with ⋃₀. -/
303  theorem dense_sUnion_interior_of_closed {S : set (set α)} (hc : ∀s∈S, is_closed s)
id                                                └─┘  └─┘              └───────┘ 
src                                               └─┘  └─┘                 └───────┘
typ                                               └─┘  └─┘              └───────┘ 
doc                                                                        └───────┘
304    (hS : countable S) (hU : (⋃₀ S) = univ) : closure (⋃s∈S, interior s) = univ :=
id           └───────┘          └┘    └──┘    └─────┘    └──────┘    └──┘
src          └───────┘           └┘     └──┘    └─────┘      └──────┘     └──┘
typ          └───────┘          └┘    └──┘    └─────┘    └──────┘    └──┘
doc          └───────┘                           └─────┘      └──────┘
305  by rw sUnion_eq_bUnion at hU; exact dense_bUnion_interior_of_closed hc hS hU
id         └──────────────┘              └─────────────────────────────┘ └┘ └┘ └┘
src     └─┘└──────────────┘└────┘  └────┘└─────────────────────────────┘      
typ     └─┘└──────────────┘└────┘  └────┘└─────────────────────────────┘└┘└┘└┘
doc     └─┘                └────┘  └────┘└─────────────────────────────┘      
txt     └─┘                └────┘  └────┘                                     
par     └─┘                └────┘  └────┘                                     
pid                       └────┘                                            
st     └──────────────────────────────────────────────────────────────────────────
306  
src  
typ  
doc  
txt  
par  
pid  
st   
307  /-- Baire theorem: if countably many closed sets cover the whole space, then their interiors
308  are dense. Formulated here with an index set which is an encodable type. -/
309  theorem dense_Union_interior_of_closed [encodable β] {f : β → set α} (hc : ∀s, is_closed (f s))
id                                           └───────┘           └─┘            └───────┘   
src                                          └───────┘             └─┘              └───────┘
typ                                          └───────┘           └─┘            └───────┘   
doc                                          └───────┘                              └───────┘
310    (hU : (⋃s, f s) = univ) : closure (⋃s, interior (f s)) = univ :=
id                 └──┘    └─────┘   └──────┘       └──┘
src                   └──┘    └─────┘    └──────┘         └──┘
typ                └──┘    └─────┘   └──────┘       └──┘
doc                            └─────┘    └──────┘
311  begin
st   └─────
312    rw ← bUnion_univ,
id          └─────────┘
src    └───┘└─────────┘
typ    └───┘└─────────┘
doc    └───┘
txt    └───┘
par    └───┘
pid      └─┘
st   ─────────────────┘└─
313    apply dense_bUnion_interior_of_closed,
id           └─────────────────────────────┘
src    └────┘└─────────────────────────────┘
typ    └────┘└─────────────────────────────┘
doc    └────┘└─────────────────────────────┘
txt    └────┘
par    └────┘
pid         
st   ──────────────────────────────────────┘└─
314    { simp [hc] },
id             └┘
src      └────┘  └┘
typ      └────┘└┘└┘
doc      └────┘  └┘
txt      └────┘  └┘
par      └────┘  └┘
pid            
st   ───┘└────────┘└┘
315    { apply countable_encodable },
id             └─────────────────┘
src      └────┘└─────────────────┘
typ      └────┘└─────────────────┘
doc      └────┘                   
txt      └────┘                   
par      └────┘                   
pid                              
st   ───┘└────────────────────────┘└┘
316    { rwa ← bUnion_univ at hU }
id             └─────────┘
src      └────┘└─────────┘└─────┘
typ      └────┘└─────────┘└─────┘
doc      └────┘           └─────┘
txt      └────┘           └─────┘
par      └────┘           └─────┘
pid         └─┘           └────┘
st   ───────────────────────────┘└─
317  end
st   ──┘
318  
319  /-- One of the most useful consequences of Baire theorem: if a countable union of closed sets
320  covers the space, then one of the sets has nonempty interior. -/
321  theorem nonempty_interior_of_Union_of_closed [nonempty α] [encodable β] {f : β → set α}
id                                                 └──────┘    └───────┘           └─┘ 
src                                                └──────┘     └───────┘             └─┘
typ                                                └──────┘    └───────┘           └─┘ 
doc                                                             └───────┘
322    (hc : ∀s, is_closed (f s)) (hU : (⋃s, f s) = univ) : ∃s x ε, ε > 0 ∧ ball x ε ⊆ f s :=
id              └───────┘                  └──┘            └──┘     
src              └───────┘                       └──┘                └──┘     
typ             └───────┘                  └──┘            └──┘     
doc              └───────┘                                                └──┘
323  begin
st   └─────
324    have : ∃s, (interior (f s)).nonempty,
id               └──────┘  
src    └─────┘ └──────┘   └─────────┘
typ    └─────┘ └──────┘  └─────────┘
doc    └─────┘   └──────┘   └─────────┘
txt    └─────┘              └─────────┘
par    └─────┘              └─────────┘
pid    └───┘└┘              └────────┘
st   ─────────────────────────────────────┘└─
325    { by_contradiction h,
src      └────────────────┘
typ      └────────────────┘
doc      └────────────────┘
txt      └────────────────┘
par      └────────────────┘
pid                      └┘
st   ───┘└────────────────┘└─
326      simp only [not_exists, not_nonempty_iff_eq_empty] at h,
id                  └────────┘  └───────────────────────┘
src      └─────────┘└────────┘└┘└───────────────────────┘└────┘
typ      └─────────┘└────────┘└┘└───────────────────────┘└────┘
doc      └─────────┘          └┘                         └────┘
txt      └─────────┘          └┘                         └────┘
par      └─────────┘          └┘                         └────┘
pid          └──┘└┘          └┘                         └──┘
st   ─────────────────────────────────────────────────────────┘└─
327      have := calc ∅ = closure (⋃s, interior (f s)) : by simp [h]
id                       └─────┘    └──────┘                  
src      └──────┘     └─────┘ └──────┘   └───┘  └────┘ └─
typ      └──────┘     └─────┘ └──────┘  └───┘  └────┘└─
doc      └──────┘      └─────┘ └──────┘   └───┘  └────┘ └─
txt      └──────┘                           └───┘  └────┘ └─
par      └──────┘                           └───┘  └────┘ └─
pid      └───┘└─┘                           └───┘  └─────┘ └─
st   ─────────────────────────────────────────────────────┘└─────────
328                   ... = univ : dense_Union_interior_of_closed hc hU,
id                          └──┘   └────────────────────────────┘ └┘ └┘
src  ────────────────┘└──┘ └──┘└─┘└────────────────────────────┘  
typ  ────────────────┘└──┘ └──┘└─┘└────────────────────────────┘└┘└┘
doc  ────────────────┘└──┘     └─┘└────────────────────────────┘  
txt  ────────────────┘└──┘     └─┘                                
par  ────────────────┘└──┘     └─┘                                
pid  ────────────────────┘     └─┘                                
st   ────────────────┘└───────────────────────────────────────────────┘└─
329      exact univ_nonempty.ne_empty this.symm },
id             └────────────────────┘ └───────┘
src      └────┘└────────────────────┘└───────┘
typ      └────┘└────────────────────┘└───────┘
doc      └────┘                               
txt      └────┘                               
par      └────┘                               
pid                                          
st   ──────────────────────────────────────────┘└┘
330    rcases this with ⟨s, hs⟩,
id            └──┘
src    └─────┘    └───────────┘
typ    └─────┘└──┘└───────────┘
doc    └─────┘    └───────────┘
txt    └─────┘    └───────────┘
par    └─────┘    └───────────┘
pid              └───────────┘
st   ─────────────────────────┘└─
331    rcases hs with ⟨x, hx⟩,
id            └┘
src    └─────┘  └───────────┘
typ    └─────┘└┘└───────────┘
doc    └─────┘  └───────────┘
txt    └─────┘  └───────────┘
par    └─────┘  └───────────┘
pid            └───────────┘
st   ───────────────────────┘└─
332    rcases mem_nhds_iff.1 (mem_interior_iff_mem_nhds.1 hx) with ⟨ε, εpos, hε⟩,
id            └──────────┘    └───────────────────────┘   └┘
src    └─────┘└──────────┘└─┘ └───────────────────────┘└─┘  └──────────────────┘
typ    └─────┘└──────────┘└─┘ └───────────────────────┘└─┘└┘└──────────────────┘
doc    └─────┘            └─┘                          └─┘  └──────────────────┘
txt    └─────┘            └─┘                          └─┘  └──────────────────┘
par    └─────┘            └─┘                          └─┘  └──────────────────┘
pid                      └─┘                          └─┘  └──────────────────┘
st   ──────────────────────────────────────────────────────────────────────────┘└─
333    exact ⟨s, x, ε, εpos, hε⟩,
id                  └──┘  └┘
src    └────┘  └┘ └┘ └┘    └┘  
typ    └────┘ └┘└┘└┘└──┘└┘└┘
doc    └────┘  └┘ └┘ └┘    └┘  
txt    └────┘  └┘ └┘ └┘    └┘  
par    └────┘  └┘ └┘ └┘    └┘  
pid           └┘ └┘ └┘    └┘  
st   ──────────────────────────┘└─
334  end
st   ──┘
335  
336  end Baire_theorem